\begin{tabbing}
es{-}copies(${\it es}$;$e$;$x$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=$\exists$$a$:Atom1.\+
\\[0ex](\=es{-}atom(${\it es}$;es{-}loc(${\it es}$; $e$);$a$)\+
\\[0ex]$\Rightarrow$ es{-}when(${\it es}$; $x$; es{-}init(${\it es}$;$e$)):es{-}vartype(${\it es}$; es{-}loc(${\it es}$; $e$); $x$)$>>$$a$)
\-\\[0ex]\& $\neg$es{-}state{-}when{-}without(${\it es}$;$e$;$x$):es{-}state{-}without(${\it es}$;es{-}loc(${\it es}$; $e$);$x$)$>>$$a$
\\[0ex]\& $\neg$es{-}rcv{-}atom(${\it es}$;$e$;$a$)
\\[0ex]\& es{-}state{-}after{-}without(${\it es}$;$e$;$x$):es{-}state{-}without(${\it es}$;es{-}loc(${\it es}$; $e$);$x$)$>>$$a$
\-
\end{tabbing}